k:Knd, l:IdLnk. (isrcvl(l;k))  ((isrcv(k)) & lnk(k) = l) 

latex

Definitions	b, t  T, P  Q, x:A. B(x), lnk(k), s = t, , IdLnk, False, Type, x:A  B(x), P & Q, P  Q, P  Q, True, a = b, , A, b, x:AB(x), Unit, left + right, isrcvl(l;k), Knd, isrcv(k), Void, A c B
Lemmas	iff functionality wrt iff, assert-eq-lnk, IdLnk wf, Knd wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, isrcv wf, bool wf, assert wf, eq lnk wf, true wf, false wf, lnk wf